ПОДХОД К ВЕРИФИКАЦИИ АЛЛОКАТОРОВ ДИНАМИЧЕСКОЙ ПАМЯТИ, ОСНОВАННЫЙ НА СИМВОЛЬНОМ ВЫПОЛНЕНИИ ПРОГРАММ
Аннотация:
Предмет исследования. Исследованы техники эксплуатации уязвимостей в реализации алгоритмов распределения динамической памяти – аллокаторе библиотеки glibc (Poisoned Null-byte, Overlapped Chunks, Fastbin Attack, Unsafe Unlink, House of Einherjar, House of Force, House of Spirit, House of Lore, Unsorted Bin Attack). Приведены примеры кода эксплуатации уязвимостей и классификация представленных техник в соответствии с общим перечнем Common Weakness Enumeration. Исследованы современные методы и средства обнаружения уязвимостей, показаны их достоинства и недостатки на примере работы фреймворка Heap Hopper. Рассмотрены современные подходы к верификации программного обеспечения. Метод. Предложенный метод верификации программного обеспечения совмещает подходы статического анализа и символьного выполнения при использовании точной модели алгоритмов выделения динамической памяти. В процессе компиляции проверяемой программы создается структура Крипке. Уязвимости динамической памяти описываются формулами темпоральной логики. Полученная структура и формулы передаются на вход алгоритма проверки моделей. Осуществляется конкретно-символьное выполнение собранного бинарного файла. Для символьных путей выполнения проверяются условия уязвимостей, выраженные в виде формул пропозициональной логики. Основные результаты. Показана возможность практического применения предложенного подхода к обнаружению уязвимостей, возникающих при распределении динамической памяти в программных приложениях. Символьное выполнение реализовано в виде низкоуровневого отладчика, что позволяет снизить время работы алгоритмов за счет выполнения проверяемого приложения на реальном процессоре. Практическая значимость. Представлен комплексный подход для решения проблемы автоматического выявления уязвимостей на разных стадиях жизненного цикла разработки программного обеспечения. Предложенный подход применим для верификации аналогичных реализаций аллокаторов динамической памяти, таких как ptmalloc, dlmalloc, tcmalloc, jemalloc, musl.
Ключевые слова:
Постоянный URL
Статьи в номере
- ПРИМЕНЕНИЕ РАДИОФОТОНИКИ В ВОЛОКОННО-ОПТИЧЕСКИХ ИЗМЕРИТЕЛЬНЫХ ПРИБОРАХ
- ОПТИКО-ЭЛЕКТРОННЫЙ КОМПЛЕКС ДЕТАЛЬНОГО НАБЛЮДЕНИЯ
- ТЕОРЕТИЧЕСКАЯ МОДЕЛЬ ИЗМЕНЕНИЯ ЦВЕТА РЕДУКТАЗНОЙ ПРОБЫ С РЕЗАЗУРИНОМ КАК ОСНОВА КОНТРОЛЯ КАЧЕСТВА МОЛОКА В ПРОЦЕССЕ ЕГО ХРАНЕНИЯ
- ЮСТИРОВКА ПЕРЕДАЮЩЕГО КАНАЛА ЛАЗЕРНОЙ ЛОКАЦИОННОЙ СИСТЕМЫ
- МЕТОД ВЫЧИСЛЕНИЯ ЭНЕРГОЭФФЕКТИВНОСТИ ГАЗОРАЗРЯДНЫХ ИМПУЛЬСНЫХ ЛАМП
- ИССЛЕДОВАНИЕ ВЛИЯНИЯ РЕЖИМОВ 3D-ПЕЧАТИ КЕРАМИКОЙ И СИНТЕРИЗАЦИИ НА ПРОЦЕСС УСАДКИ ТОНКОСТЕННЫХ ДЕТАЛЕЙ
- ИССЛЕДОВАНИЕ ЭНЕРГЕТИЧЕСКИХ ХАРАКТЕРИСТИК УГЛЕРОДОСОДЕРЖАЩЕГО КОМПОЗИТНОГО МАТЕРИАЛА ТЕПЛОЭЛЕКТРОНАКОПИТЕЛЯ
- МЕТОДИКА ДИФФЕРЕНЦИРОВАННОГО НАРАЩИВАНИЯ ЕМКОСТИ СИСТЕМЫ ХРАНЕНИЯ ДАННЫХ С МНОГОУРОВНЕВОЙ СТРУКТУРОЙ
- БЫСТРЫЙ АЛГОРИТМ ВНУТРИКАДРОВОГО КОДИРОВАНИЯ ДЛЯ HEVC НА ОСНОВЕ ВЕРОЯТНОСТИ ВЫБОРА РЕЖИМА
- АНАЛИЗ ПЕРСПЕКТИВНОГО РАЗВИТИЯ ЭНЕРГЕТИЧЕСКИХ СИСТЕМ В УСЛОВИЯХ ЦИФРОВОЙ ТРАНСФОРМАЦИИ РОССИЙСКОЙ ЭКОНОМИКИ
- АВТОМАТИЗАЦИЯ ПОСТРОЕНИЯ СРЕДСТВ ДИАГНОСТИРОВАНИЯ ДЛЯ ПОТОКОВОЙ ВЫЧИСЛИТЕЛЬНОЙ СИСТЕМЫ РЕАЛЬНОГО ВРЕМЕНИ
- МАТЕМАТИЧЕСКОЕ МОДЕЛИРОВАНИЕ РАЗНИЦЫ УГЛОВ НАПРАВЛЕНИЯ ЗУБЬЕВ В ЗОНЕ ЗАЦЕПЛЕНИЯ И ПОЛНОТА КОНТАКТА В ЗУБЧАТЫХ ПЕРЕДАЧАХ
- ПРОГНОЗИРОВАНИЕ РЕАКЦИИ ПОЛЬЗОВАТЕЛЕЙ В СОЦИАЛЬНЫХ СЕТЯХ МЕТОДАМИ МАШИННОГО ОБУЧЕНИЯ
- МОДЕЛИРОВАНИЕ ПЕРЕХОДНЫХ ПРОЦЕССОВ В СИЛОВЫХ ПРЕОБРАЗОВАТЕЛЯХ, ПИТАЮЩИХСЯ ОТ ОБЩЕГО ЗВЕНА ПОСТОЯННОГО ТОКА
- МЕТОДИКА ОПТИМИЗАЦИИ УСТРОЙСТВА НАКОПЛЕНИЯ ЭНЕРГИИ В ПЕРИФЕРИЙНОМ СТЫКОВОЧНОМ АГРЕГАТЕ
- ОСРЕДНЕНИЕ УРАВНЕНИЙ ДВИЖЕНИЯ В ПОТЕНЦИАЛЬНЫХ АВТОНОМНЫХ СИСТЕМАХ
- СРАВНИТЕЛЬНЫЙ АНАЛИЗ ПРОСТРАНСТВЕННЫХ ХАРАКТЕРИСТИК ДВУХЭЛЕМЕНТНЫХ МИКРОФОННЫХ РЕШЕТОК
- МОДЕЛИРОВАНИЕ СОСТОЯНИЯ ПОВЕРХНОСТИ МЕМБРАНЫ ПРИ ТОЧЕЧНОМ ВОЗДЕЙСТВИИ
- ПАМЯТИ ЮРИЯ ГРИГОРЬЕВИЧА ЯКУШЕНКОВА